FDL - Nuprl Lemma : union-decodes_wf

Nuprl Lemma : union-decodes_wf

es:ES, C, T:Type, R1, R2:(C

E

), decodes1:(i:C

e:{x:E| R1(i,x)}

state@loc(e)

T),

decodes2:(i:C

e:{x:E| R2(i,x)}

state@loc(e)

T), dec_R1:(i:C

e:E

Dec(R1(i,e))).
[R1 ? decodes1 : decodes2]

i:C

e:{x:E| (R1(i,x))

(R2(i,x))}

state@loc(e)

T

Definitions P Q, left + right, Dec(P), {x:A| B(x)} , f(a), state@i, loc(e), x:AB(x), E, x:A. B(x), , Type, t T, ES, [R ? decodes1 : decodes2], x.A(x), if p:P then A(p) else B fi , s = t, P Q, A, False

Lemmas event system wf, es-E wf, es-loc wf, es-state wf, decidable wf